ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), m:, L:(event-info(ds;da) List).
(ecl-act(ds; da; m; x)(L))
 (L':(event-info(ds;da) List), n:.
 iseg(event-info(ds;da); L'; L)  (ecl-halt(ds; da; x)(n,L'))  (L = L')) 

latex

Definitions

x:A. B(x), P  Q, ecl-act(ds; da; m; x), ecl-halt(ds; da; x), prop{i:l}, t  T, x. t(x), , P  Q, x:A. B(x), P  Q, A  B, A, False, iseg(T; l1; l2), P  Q, P  Q, T, True, top, subtype(S; T), , guard(T), ge(i; j), compat(T; l1; l2), ||as||, Y, sq_type(T), x(s), decidable(P), star-append(T; P; Q), append(as; bs), concat(ll), reduce(f; k; as), if b then t else f fi , tt, ff, l_exists(L; T; x.P(x))

Lemmas

ecl-induction, nat wf, event-info wf, ecl-act wf, iseg wf, ecl-halt wf, ecl wf, fpf wf, Knd wf, Id wf, false wf, decl-state wf, ma-valtype wf, bool wf, append wf, le wf, ecl-halt-unique, common iseg compat, length wf1, non neg length, iseg append0, member wf, append assoc, iseg length, length append, squash wf, true wf, append nil sq, top wf, iseg transitivity, append iseg, decidable lt, iseg antisymmetry, nat plus wf, nat plus inc, star-append wf, concat wf, l all wf, nat properties, ge wf, l all cons, compat wf, compat-append, length-append, ecl-halt-nil, bool cases, bool sq, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, ifthenelse wf, eq int wf, l member wf, l exists wf